%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "En un edificio de tres plantas viven Daniel, Jaime y Andrés. Todos los
% habitantes de la primera planta conocen a todos los de la tercera. Jaime sólo
% conoce a habitantes de la segunda y la tercera plantas. Andrés no vive en la
% segunda planta y no conoce a nadie de la tercera planta. Jaime vive en la
% segunda planta y conoce a Daniel. Por tanto Daniel vive en la segunda
% planta."

%==============================================================================
% Formalización
%==============================================================================

set(binary_res).

formula_list(sos).
  edificio(Daniel).
  edificio(Andres).
  edificio(Jaime).

  all x (edificio(x) -> primera(x) | segunda(x) | tercera(x)).

% all x y (primera(x) & primera(y) -> conoce(x,y)).
% all x y (segunda(x) & segunda(y) -> conoce(x,y)).
% all x y (tercera(x) & tercera(y) -> conoce(x,y)).

  all x y (conoce(x,y) -> conoce(y,x)).

  all x (conoce(x,x)).

% Todos los habitantes de la primera planta conocen a todos los de la tercera.
  all x (primera(x) -> (all y (tercera(y) -> conoce(x,y)))).

% Jaime sólo conoce a habitantes de la segunda y la tercera plantas.
  all x (conoce(Jaime,x) -> segunda(x) | tercera(x)).

% Andrés no vive en la segunda planta y no conoce a nadie de la tercera planta.
  - segunda(Andres).
  all x (conoce(Andres,x) -> (- tercera(x))).

% Jaime vive en la segunda planta y conoce a Daniel.
  segunda(Jaime) & conoce(Jaime,Daniel).

% Conclusión: Daniel vive en la segunda planta.
  - segunda(Daniel).

end_of_list.

%==============================================================================
